nats → adx(zeros)
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
hd(cons(X, Y)) → activate(X)
tl(cons(X, Y)) → activate(Y)
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(X)
activate(n__adx(X)) → adx(X)
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
nats → adx(zeros)
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
hd(cons(X, Y)) → activate(X)
tl(cons(X, Y)) → activate(Y)
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(X)
activate(n__adx(X)) → adx(X)
activate(X) → X
INCR(cons(X, Y)) → ACTIVATE(Y)
ADX(cons(X, Y)) → ACTIVATE(X)
ADX(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(X)) → INCR(X)
NATS → ZEROS
NATS → ADX(zeros)
ACTIVATE(n__s(X)) → S(X)
HD(cons(X, Y)) → ACTIVATE(X)
TL(cons(X, Y)) → ACTIVATE(Y)
INCR(cons(X, Y)) → ACTIVATE(X)
ACTIVATE(n__0) → 01
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(X)) → ADX(X)
ACTIVATE(n__zeros) → ZEROS
nats → adx(zeros)
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
hd(cons(X, Y)) → activate(X)
tl(cons(X, Y)) → activate(Y)
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(X)
activate(n__adx(X)) → adx(X)
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
INCR(cons(X, Y)) → ACTIVATE(Y)
ADX(cons(X, Y)) → ACTIVATE(X)
ADX(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(X)) → INCR(X)
NATS → ZEROS
NATS → ADX(zeros)
ACTIVATE(n__s(X)) → S(X)
HD(cons(X, Y)) → ACTIVATE(X)
TL(cons(X, Y)) → ACTIVATE(Y)
INCR(cons(X, Y)) → ACTIVATE(X)
ACTIVATE(n__0) → 01
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(X)) → ADX(X)
ACTIVATE(n__zeros) → ZEROS
nats → adx(zeros)
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
hd(cons(X, Y)) → activate(X)
tl(cons(X, Y)) → activate(Y)
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(X)
activate(n__adx(X)) → adx(X)
activate(X) → X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
ADX(cons(X, Y)) → ACTIVATE(X)
INCR(cons(X, Y)) → ACTIVATE(Y)
ADX(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(X)) → INCR(X)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(X)) → ADX(X)
INCR(cons(X, Y)) → ACTIVATE(X)
nats → adx(zeros)
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
hd(cons(X, Y)) → activate(X)
tl(cons(X, Y)) → activate(Y)
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(X)
activate(n__adx(X)) → adx(X)
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ADX(cons(X, Y)) → ACTIVATE(X)
ADX(cons(X, Y)) → ACTIVATE(Y)
Used ordering: Polynomial interpretation [25,35]:
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(X)) → INCR(X)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(X)) → ADX(X)
INCR(cons(X, Y)) → ACTIVATE(X)
The value of delta used in the strict ordering is 1/4.
POL(n__incr(x1)) = (1/4)x_1
POL(ADX(x1)) = 1/4 + (1/4)x_1
POL(n__adx(x1)) = 1/4 + (1/4)x_1
POL(n__zeros) = 0
POL(activate(x1)) = x_1
POL(n__s(x1)) = 0
POL(0) = 0
POL(cons(x1, x2)) = (4)x_1 + (4)x_2
POL(adx(x1)) = 1/4 + (1/4)x_1
POL(incr(x1)) = (1/4)x_1
POL(zeros) = 0
POL(n__0) = 0
POL(s(x1)) = 0
POL(INCR(x1)) = (1/4)x_1
POL(ACTIVATE(x1)) = x_1
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
zeros → cons(n__0, n__zeros)
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
s(X) → n__s(X)
zeros → n__zeros
adx(X) → n__adx(X)
incr(X) → n__incr(X)
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__incr(X)) → incr(X)
activate(n__s(X)) → s(X)
activate(X) → X
activate(n__adx(X)) → adx(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(X)) → INCR(X)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(X)) → ADX(X)
INCR(cons(X, Y)) → ACTIVATE(X)
nats → adx(zeros)
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
hd(cons(X, Y)) → activate(X)
tl(cons(X, Y)) → activate(Y)
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(X)
activate(n__adx(X)) → adx(X)
activate(X) → X